Nuprl Lemma : rel-immediate-exists 11,40
T:Type, R:(TT).
SWellFounded(R(x,y))
 (x, y:T. Dec(z:T. (R(x,z) & R(z,y))))
 (y:T. (x:T. (R(x,y)))  (x:T. (R!(x,y)))) 
latex

Definitionst  T, P  Q, x:A. B(x), R!, f(a), x:A  B(x), x:A. B(x), P & Q, Dec(P), x:AB(x), SWellFounded(R(x;y)), Type, , R^+, x f y, R1 => R2, P  Q
Lemmasrel plus iff, rel-immediate wf, rel-rel-plus, rel-immediate-rel-plus

origin